Search for: All records

Specifying and verifying the temporal properties of UML-based systems can be challenging. Although there exist some extensions of OCL to support the specification of temporal properties in UML-based notations, most of the approaches depend on using non-UML formal formalisms such as LTL, CTL, and CTL* while transforming the under-development UML models into non-UML model checking frameworks for verification. This approach introduces complexities and relies on techniques and tools that are not within the UML spectrum. In this paper, we show how TOCL (one OCL extension for temporal properties specification) can be transformed into OCL for verification purposes. Towards this end, we created a formal EBNF grammar for TOCL, based on which a parser and a MOF metamodel were generated for the language. Additionally, to facilitate the analysis of the TOCL properties, we formally defined transformation rules from TOCL metamodel to OCL metamodel using QVT. Finally, we validated the implementations of the transformation rules using USE. 

In this work we present a process and a tool to apply formal methods in Internet of Things (IoT) applications using the Unified Modeling Language (UML). As there are no best practices to develop secured IoT systems, we have developed a plug-in tool that integrates a framework to validate UML software models and we present the design of a location-based IoT application as a use case for the validation tool.